/******************************************************
Compile : gcc -O3 -o infer4 infer4.c io.c ksat.c enhance-sim.c sat-utils.c utils.c wrapper-minisat.c solver.c solver-utils.c -lm
******************************************************/

#include "infer.h"
#include "ksat.h"
#include "wrapper-minisat.h"
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <sys/time.h> 

void print_help ()
{
	printf ("Usage          : ./infer4 inputfile trigger model steps links\n");
	printf ("                (./infer4 input1 1 3 -1 -1)\n\n");
	printf ("trigger        : 1 first node is a trigger node\n");
	printf ("model          : 0 SIM; 1 SIM + Reliable Trans; 2 SIM + Convergence; 3 SIM + Reliable Trans + Convergence\n");
	printf ("steps          : number of steps (positive: fixed steps; negative: variable steps; -1: no restriction)\n");
	printf ("links          : the maximum of the number of interactions (positive: pattern; negative: one solution)\n\n");
	printf ("Note           : This program will generate the pattern of qualified networks and one qualified process\n\n");
}

void do_infer (struct infer *infer)
{
	int i, j, N, L, M;

	N = infer->N;
	L = infer->L;

	if (L > 0)
		infer->fixL = 1;
	else
		infer->fixL = 0;

	if (L == -1)
		L = infer->maxL;
	else if (L < 0)
		L = -L;

	int pathway[L][N], R1[N + 1];
	int S[L][N]; /* state variable */
	int g[N][N], r[N][N]; /* network variable ; g[i][j]/r[i][j] edge from j to i */

	init_pathway (N, L, pathway, infer);

	struct ksat *ksat;

	ksat = setup_ksat (N, L, pathway, S, g, r, infer);

	bool st;
	int list[ksat->num_variables + 1];

	if (infer->links > 0)
	{
		for (i = 1; i < ksat->num_variables + 1; i++)
		{
			list[i] = 0;
		}
		for (i = 0; i < N; i++)
		{
			for (j = 0; j < N; j++)
			{
				list[r[i][j]] = 1;
				list[g[i][j]] = 1;
			}
		}
        
		st = solve_ksat2 (ksat, list);
	}
	else
		st = solve_ksat1 (ksat, list);

	if (st == true)
	{
		for (i = 1; i < L - 2; i++)
		{
			for (j = 0; j < N; j++)
			{
				pathway[i][j] = list[S[i][j]];
			}
		}

		if (infer->fixL == 0)
		{
			for (i = L - 2; i > 0; i--)
			{
				for (j = 0; j < N; j++)
				{
					if (pathway[i][j] != pathway[i - 1][j])
						break;
				}
				if (j != N)
				{
					L = infer->L = i + 2;
					break;
				}
			}
		}

		print_pathway (N, L, pathway);
		infer->links = print_network (N, g, r, list);
	}
	else
	{
		infer->L = 0;
		infer->links = 0;
		printf ("No solution!\n");
	}

	free_ksat (ksat);
}

int main (int argc, char *argv[])
{
	int i, links;
	struct infer infer;
	struct timeval tpstart,tpend;
	float timeuse;

	if (argc == 1)
	{
		print_help ();
		exit (0);
	}

	gettimeofday (&tpstart,NULL);

	read_inputfile (argv[1], &infer);
	infer.trigger = atoi (argv[2]);
	infer.model = atoi (argv[3]);
	infer.L = atoi (argv[4]);
	infer.links = atoi (argv[5]);

	do_infer (&infer);

	gettimeofday(&tpend,NULL); 
	timeuse = 1000000 * (tpend.tv_sec-tpstart.tv_sec) + tpend.tv_usec-tpstart.tv_usec; 
	timeuse /= 1000000; 

	int flips;

	flips = 0;
	for (i = 0; i < infer.N; i++)
	{
		flips += infer.flips[i];
	}

	printf("Used Time : %8.2f\tNumber of flips : %2d %2d\tNumber of steps : %2d\tNumber of links : %2d\n", timeuse, flips, infer.flips[infer.N], infer.L, infer.links);
}
